Nuprl Lemma : bframe-p_wf
0,22
postcript
pdf
es
:ES,
i
:Id,
k
:Knd,
L
:IdLnk List. @
i
:
k
sends only on links in
L
Prop
latex
Definitions
t
T
,
{
x
:
A
|
B
(
x
) }
,
(Msg on
l
)
,
ES
,
Id
,
Knd
,
IdLnk
,
type
List
,
Msg
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
loc(
e
)
,
s
=
t
,
E
,
nil
,
S
T
,
sends(
l
;
e
)
,
Prop
,
(
x
l
)
,
A
,
P
Q
,
kind(
e
)
,
x
.
t
(
x
)
,
e
@
i
.
P
(
e
)
,
@
i
:
k
sends only on links in
L
Lemmas
alle-at
wf
,
es-kind
wf
,
not
wf
,
l
member
wf
,
es-sends
wf
,
es-Msgl
wf
,
es-Msg
wf
,
es-E
wf
,
es-loc
wf
,
IdLnk
wf
,
Knd
wf
,
Id
wf
,
event
system
wf
origin
es:ES, i:Id, k:Knd, L:IdLnk List. @i:k sends only on links in L 
Prop es:ES, i:Id, k:Knd, L:IdLnk List. @i:k sends only on links in L Prop T
B(x)x:A. B(x)
T l)
A
Q
x. t(x)e@i. P(e)